r, s:. Dec(r = s) 

latex

Definitions	ff, A, P  Q, , tt, P  Q, , if b then t else f fi , Dec(P), t  T, x:A. B(x), False, P & Q, P  Q, Unit,
Lemmas	not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, false wf, assert-qeq, eqtt to assert, assert wf, iff transitivity, bool wf, qeq wf2, rationals wf